| Definitions |  x:A. B(x), P   Q, Normal(T), A & B, P & Q, t  T, DeclaredType(ds;x),   x. t(x), if b t else f fi, true, Top, Prop, State(ds), f || g, SQType(T), {T}, false, A || B, Y, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), True, R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), p  q, i=j, 1of(t), 2of(t), Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1),  A, b, l[i], {i..j }, ||as||, i  j < k, AB, False, hd(l), nth_tl(n;as), ij, i<j, P  Q,  x:A. B(x), P Q, state@i, e@i. P(e),  b, P  Q,  T, Id, R ||- es.P(es), x(s),  , Unit, (e <loc e'), @i x initially v:T, @i events of kind k change x to f State(ds) (val:T), @i only events in L change x : T, Dec(P), State(ds),  , R-base-recognize(i;ds;x;k;T;test), x when e, s.x |
| Lemmas | R-init-rule, bool wf, bfalse wf, R-frame-rule, bool-inhabited, R-effect-rule, fpf-join wf, fpf-single wf, fpf-join-cap-sq, top wf, fpf-cap-single, fpf-single-dom-sq, eqof eq btrue, ifthenelse wf, btrue wf, fpf-cap-single-join, normal-ds-join, normal-ds-single, normal-ds wf, normal-type wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, not wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, decl-state wf, Knd wf, fpf wf, ma-state-subtype, fpf-sub-join-right, fpf-single-dom, Id sq, R-and-rule, Rinit wf, Rframe wf, init-p wf, event system wf, frame-p wf, eq id wf, iff transitivity, eqtt to assert, assert-eq-id, fpf-compatible-self, fpf-empty-compatible-right, Kind-deq wf, fpf-empty wf, bnot wf, eqff to assert, assert of bnot, not functionality wrt iff, Rplus wf, Reffect wf, decl-type wf, fpf-cap wf, effect-p wf, R-compat-Rplus-sq, fpf-compatible-join, fpf-compatible-single2, fpf-empty-compatible-left, select member, le wf, R-implies-rule, R-base-recognize wf, es-vartype wf, es-state wf, es-kindtype wf, alle-at wf, iff wf, es-E wf, es-locl wf, es-kind wf, es-loc wf, es-when wf, es-state-when wf, es-loc-pred, es-locl-iff, es-val wf, es-valtype-kindtype, Knd sq, vartype-es-state-sub, alle-at-iff, subtype rel dep function, subtype rel self, subtype rel transitivity, subtype-fpf-cap-top, bool sq, es-first wf, es-when-first, false wf, es-first-implies, decidable equal Kind, es-pred wf, es-after wf, es-after-pred, bool cases, fpf-cap-single1, true wf, es-pred-locl, squash wf, es-valtype wf, l member wf, member singleton |
Type, x:Id, k:Knd, T:Type, test:(State(ds)
